Inference at * 
Iof proof for Lemma multiply functionality wrt le:


  i1, i2, j1, j2:. (i1  j1)  (i2  j2)  ((i1 * i2)  (j1 * j2)) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term) 

latex

 1: 

 1: 1. i1 : 
 1: 2. i2 : 
 1: 3. j1 : 
 1: 4. j2 : 
 1: 5. i1  j1
 1: 6. i2  j2
 1:   (i1 * i2)  (j1 * j2)
 .

Definitions	t  T, P  Q, x:A. B(x), ,
Lemmas	nat wf, le wf